Lemma xyz:
  forall (f: Prop -> Prop) x y z,
    x = y -> y = z -> f x = f z.
Proof.
  intros.
  cut (x = z).
  - intros. subst. reflexivity.
  - subst. reflexivity.
Qed.